basic
\\[0ex]Inverse($T$;${\it op}$;${\it id}$;${\it inv}$) $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$$\forall$$x$:$T$. ($x$ ${\it op}$ (${\it inv}$($x$))) = ${\it id}$ \& ((${\it inv}$($x$)) ${\it op}$ $x$) = ${\it id}$